COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	basic facts about arithmetic and proofs by Bellin
C00007 00003	inductive principles
C00014 ENDMK
C⊗;
;basic facts about arithmetic and proofs by Bellin

(wipe-out)  
(proof natnum)

(decl lessp (type: |ground⊗ground→truthval|) (syntype: constant) (infixname: <)
      (bindingpower: 920))
(decl add1 (type: |ground→ground|) (syntype: constant) (postfixname: |'|)
      (bindingpower: 975))
(decl plus (infixname: |+|) (type: |ground⊗ground⊗ground*→ground|) (syntype: constant)
      (associativity: both) (bindingpower: 930))    
(decl times (type: |ground⊗ground⊗ground*→ground|) (syntype: constant)
      (infixname: |*|) (associativity: both)(bindingpower: 935))

(decl (i j k n m) (sort: natnum) (type: ground))
(decl (a b c set) (type: |ground→truthval|))

;needed axioms on order

(axiom |∀n.¬n<n|)
(label irreflexivity_of_order)

(axiom |∀n m k.n<m∧m<k⊃n<k|)
(label transitivity_of_order)

(axiom |∀n.¬n<0|)
(label zeroleast1)

;successor and order

(axiom |∀n.natnum(n')|)
(label simpinfo)

(axiom |∀n.n<n'|)
(label successor1) (label succfacts)

(axiom |∀n m.¬n<m⊃m<n'|)
(label successor2) (label succfacts)
 
(axiom |∀n m.n'<m'≡n<m|)
(label successorless) (label succfacts)

(axiom |∀n m.(n'=m')≡(n=m)|)
(label successoreq) (label succfacts)

(axiom |∀n.¬n=0⊃0<n|)
(label zeroleast2) (label succfacts)
 
(axiom |∀n.0<n'|)
(label zeroleast3) (label succfacts)

(axiom  |∀n.¬(n'=0)|)
(label zero_not_successor) (label succfacts)

;definition of predecessor

(decl pred (type: |ground→ground|) (syntype: constant))
(defax pred |∀n.pred(n')=n|)
(label simpinfo)

(axiom |∀n.natnum pred n|)
(label simpinfo)

;addition

(defax plus |∀n k.0+n=n∧k'+n=(k+n)'|)
(label simpinfo) (label plusfacts)

(axiom |∀n m.natnum(n+m)|)
(label simpinfo)

(axiom |∀n.n+0=n|)
(label simpinfo) (label plusfacts)

(axiom |∀n.1+n=n'∧n+1=n'|)
(label simpinfo) (label plusfacts) (label plusdef1)

(axiom |∀n k.n+k'=(n+k)'|)
(label simpinfo) (label plusfacts)

(axiom |∀n k m.(k+m=k+n)≡(m=n)|)
(label lpluscan) (label plusfacts)

(axiom |∀n k m.(m+k=n+k)≡(m=n)|)
(label rpluscan) (label plusfacts)

(axiom |∀n k.n+k=0≡n=0∧k=0|)
(label addtozero) (label plusfacts)

;the effect of the following axiom is to force sums in basically normal
;form: the "simpler" terms will come first

(axiom |∀k n.k+n=n+k|)
(label commutadd) (label plusfacts)

;multiplication

(defax times |∀n k.0*n=0∧n'*k=(n*k)+k|)
(label simpinfo) (label timesfacts) (label timesdef)

(axiom |∀n m.natnum(m*n)|)
(label simpinfo)
  
(axiom |∀n.n*0=0∧1*n=n∧n*1=n|)
(label simpinfo) (label timesfacts)

(axiom |∀n k.n*k'=n*k+n|)
(label timsucc) (label timesfacts)

(axiom |∀n k m.¬k=0⊃((k*m=k*n)≡(m=n))|)
(label ltimescan) (label timesfacts)

(axiom |∀n k m.¬k=0⊃((m*k=n*k)≡(m=n))|)
(label rtimescan) (label timesfacts)
 
(axiom |∀n m.n*m=m*n|)
(label commutmult) (label timesfacts)

(axiom |∀n k.¬n=0⊃n*k=0≡k=0|)
(label ltimestozero) (label timesfacts)

(axiom |∀n k.¬n=0⊃k*n=0≡k=0|)
(label rtimestozero) (label timesfacts)

;distributivity

(axiom |∀n k m.n*(k+m)=n*k+n*m|) 
(label ldistrib) (label timesfacts) (label plusfacts)

(axiom |∀n m k.(m+k)*n=m*n+k*n|)
(label rdistrib) (label timesfacts) (label plusfacts)
;inductive principles

(proof induction)

(axiom |∀a.a(0)∧(∀n.a(n)⊃a(n'))⊃(∀n.a(n))|)
(label proof_by_induction)

(decl npars (type: |ground*|))
(decl ndf (type: |ground⊗ground*→ground*|))
(decl zcase (type: |ground*→ground|))
(axiom
 |∀ndf zcase ndef.(∃fun.(∀npars n.fun(0,npars)=zcase(npars)∧
                                  fun(n',npars)=ndef(n,fun(n,ndf(n,npars)),npars)))|)
(label inductive_definition)

;the following is a form of double induction

(axiom |∀a2.(∀n m.a2(0,n)∧a2(n,0)∧(a2(n,m)⊃a2(n',m')))⊃∀n m.a2(n,m)|)
(label proof_by_doubleinduction)

;general definitional principle for inductive functions

(decl (arb arb1 arb2) (type: |?arbitrary|))
(decl indfn (type: |ground⊗@arb→@arb|))
(decl (def_fun) (type: |ground→@arb|))

;this is the primitive recursive schema for definition on  ALL
;higher type functionals:
;note the use of the variable type in declarations;
;in this way we can specialize to ANY type.

(axiom
 |∀indfn arb.∃def_fun.∀n.def_fun(0)=arb∧def_fun(n')=indfn(n,def_fun(n))|)
(label high_order_natnum_definition)

;well-foundedness

(axiom |¬∃desc.∀n.desc(n')<desc(n)|)
(label infinite_descent)

(save-proofs natnum)